1. Field of the Invention
The present invention relates generally to the field of digital system design and verification, and more particularly to an apparatus and method for identifying true and false signal paths in digital circuits.
2. Description of the Related Art
Modern digital systems contain extremely complex circuitry and have tight timing constraints. Verifying the functional and timing correctness of these systems, within the ever-shorter design cycle-time, represents a major challenge to circuit designers. Traditionally, functional and timing verifications were performed using the same tool and on the same level of design representation. In fact, in order to accurately predict timing, lower-level representations, such as gate or transistor levels, should be used. Functional verification, on the other hand, is preferably performed at higher levels of abstraction, such as RTL. Thus, from the design tool perspective, the separation of functional and timing verification enables the development of much faster and more complete algorithms for each problem.
In order to improve verification productivity, state-of-the-art verification methodologies separate the timing verification from the functional verification. Typically such a methodology uses a delay-independent functional simulation tool, or cycle-simulator, to verify the functionality of the design at the RTL level. A static timing analyzer is used to verify the timing at the gate or transistor level. An equivalence checker is then used to confirm that both tools are verifying the same logically equivalent design.
An illustration of this process is shown in FIG. 1, with respect to a sample RTL design flow. An RTL file 8 is input to a cycle simulator 2 for functional verification. The RTL file is also synthesized by a logic synthesis block 10 into a gate level design 12. The gate level design is then input to a static timer 4, along with timing control information 16, for timing verification. The static timer 4 outputs a timing report 14. Both the RTL design 8 and the gate level design 12 are input to a formal equivalence block 6 to verify that both designs are logically equivalent.
The static timing analyzer is input-vector independent and thus has a xe2x80x9ccompletenessxe2x80x9d advantage over other timing simulations. Also, by ignoring the functionality of the designs, fast graph search algorithms can be used to identify the timing critical paths. Unfortunately, the trade-off for not considering the actual logic function during timing analysis is pessimism introduced due to false paths. A false path is a circuit path that will never actually propagate a signal value or be used in the real circuit, due to the function of the combinational and/or sequential logic circuits. This pessimism can lead to over design due to optimizing for a false-path. Additionally, this optimization for a false path can lead to design trade-offs that actually worsen the true critical paths of the circuit. Consider for example the circuit of FIG. 2. The topological path delay for path c-d-e-z is 10, whereas the true path delay a-e-z is 7. If the timing is optimized based on the topological delay, then the connections between a and c are swapped, as shown in FIG. 3. After optimization, the topological delay has improved from 10 to 9, but the true delay has degraded from 7 to 8.
In further detail, existing approaches to timing verification can be grouped into three categories: Timing Simulation, Static Timing Analysis (STA), and Functional Timing Analysis (FTA). The Timing Simulation methods verify timing by simulating a circuit based on a set of input vectors specified by the circuit designer. The input vectors are applied to the circuit and responses are collected and compared to the intended results. This is the most accurate method among the existing approaches. However, there are several drawbacks to this approach, namely:
1. A set of test vectors is required, the generation of which is a labor intensive process. 2. In order to completely verify the circuit, the circuit must be simulated with all possible input vectors. Due to the tremendous number of such vectors, usually only a small portion of the set is exercised. Thus, both computation time and completeness of the verification are practical problems with this approach.
To alleviate the run time problems associated with timing simulations, other more efficient approximation methods have been proposed. At one end of the spectrum is topological timing analysis, or Static Timing Analysis (STA), an example of which is disclosed in U.S. Pat. No. 4,924,430, entitled STATIC TIMING ANALYSIS OF SEMICONDUCTOR DIGITAL CIRCUITS. This method effectively ignores the logical function of the design and assumes the worst possible delays throughout the system. Because only the topological analysis is performed for the computation, and the method is input vector independent, the STA method is very fast. Graph based algorithms can used, which are time linear with the circuit size. However, the STA method is also pessimistic since it does not take logic information into consideration, and thus the results may include false paths.
The Functional Timing Analysis criteria extend the STA method by considering both the logical behaviors and the timing characteristics of the circuits. The FTA method is based on formal methods and therefore is complete. Depending on the assumptions concerning the signal propagation criteria, the FTA method can provide accurate results. However, the FTA formulations require the solution of a Boolean satisfiability problem. The Boolean satisfiability problem is NP-complete, and thus run-time performance and memory requirements are major practical obstacles. The solution of Boolean satisfiability problems for combinational logic is well known in the art, and existing algorithms usually work well in practice. See, for example, xe2x80x9cAlgorithms for Satisfiability Problems in Combinational Switching Circuits,xe2x80x9d Joao da Silva, Ph.D. Thesis, University of Michigan, 1995. However, to correctly identify the true delay of a complex circuit, the sequential behavior of the circuit also needs to be analyzed.
Almost all of the previously proposed approaches for verification deal with combinational logic only. This implies that all possible input vectors will occur during normal system operation. In a real system, however, not all input vectors are reachable during normal system operations. For example, in FIG. 4, under normal circuit operation A and B are never at logic 1 at the same time. Accordingly, the path P-T-Z is a false path. Thus, the algorithms that rely only on the combinational logic are pessimistic (i.e. potentially too negative).
In view of the foregoing, it would be desirable to have a method and apparatus for critical and false path verification that analyzes sequential logic flow as well as combinational logic, thereby providing a more thorough, and less pessimistic, verification procedure.
In general, the present invention is an apparatus and method for identifying true and false signal paths in digital circuits. The present approach utilizes the fact that a static sensitization criteria, which may be optimistic, provides a lower bound on the true delay of a system. Since the result of the static timing analyzer is an absolute upper bound on delay, if the upper bound and lower bound are equal then a true delay has been found. When the differences between the two bounds is too large, the present invention uses the results of a floating mode algorithm as the upper bound instead.
Since it is not practically feasible to analyze false paths within a formal sequential verification framework, the present invention produces an assertion module that contains the conditions for which paths under consideration may be activated. The assertion module can then be used in conjunction with functional verification to check the validity of potentially false paths. Note that the formal approaches used in the bounded algorithm assume all input vectors are valid. Thus, if the algorithm cannot find any vector to activate a path, there is no need for further simulation.
In other words, the present invention takes all the potential false paths and captures the conditions that would make them true paths as a Boolean expression (net list), for the combinational logic only. The net list does not have to be at the gate level, but can be a simplified gate level representation because the verification process is only concerned with the logical behavior, not the actual structure. This allows the simulation to execute more quickly. Since the conditions are only captured between register elements, it can be formally proved whether or not the path can be exercised. If no register value can activate the path, then the analysis is done. Otherwise, a simulation is performed to determine whether the register values required to active the condition actually occur. If the Boolean condition can be satisfied, the simulation is performed on the sequential logic to justify those values. If the satisfiability engine fails to finish, then the simulation is run on the combinatinal logic, and an attempt is made to justify the values sequentially as well.
The present system has two main applicationsxe2x80x94(1) to verify that the false paths specified by a circuit designer are indeed false (or not true), and (2) to verify that the critical paths computed by the static timer analyzer (STA) are not false paths. Also, test vectors, at the combinational level, that can be used to exercise the critical paths are generated as a by-product. The core of the system, namely the bounded false path determination algorithm and the assertion generation, are the same for both applications.